COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 priori.lsp[s84,jmc]	ekl proof involving prioritized circumscription
C00004 ENDMK
C⊗;
;;; priori.lsp[s84,jmc]	ekl proof involving prioritized circumscription

(proof priority)

1. (define ax1 |∀ab flies.ax1(ab,flies) ≡ (∀x.¬ab aspect1 x ⊃ ¬flies x)|)

2. (define ax2 |∀ab flies.ax2(ab,flies)
	 ≡ (∀x.bird x ∧ ¬ab aspect2 x ⊃ ab aspect1 x)|)

3. (define lessp |∀ab abp.
lessp(ab,abp) ≡ (∀x.(¬ab aspect2 x ∧ abp aspect2 x)
∨ ((ab aspect2 x ≡ abp aspect2 x) ∧ ¬ab aspect1 x ∧ abp aspect1 x))|)

4. (axiom |ax1(ab0,flies0) ∧ ax2(ab0,flies0)
 ∧ (∀ab flies.ax1(ab,flies) ∧ ax2(ab,flies) ⊃ ¬lessp(ab,ab0))|)

;;; To be proved: ∀x.flies0 x ≡ bird x

lep,grosof%sumex
prioritized circumscription
priori[s84,jmc] and priori.lsp[s84,jmc] are an exposition of the
use of ordering to rehabilitate Leslie's style of axioms and an
ekl version of these axioms.  They should be looked at carefully
before anyone attempts to do the ekl proof that

(all x (equiv (flies0 x) (bird x))).

Ben, if you feel an urge to hack ekl, I'll arrange for a SAIL account.